﻿using System.Collections.Generic;
using System.IO;
using Microsoft.ExtendedReflection.Collections;
using Microsoft.ExtendedReflection.ComponentModel;
using Microsoft.ExtendedReflection.Interpretation;
using Microsoft.ExtendedReflection.Metadata;
using Microsoft.ExtendedReflection.Utilities;
using Microsoft.ExtendedReflection.Utilities.Safe.IO;
using Microsoft.Pex.Engine.ComponentModel;
using Microsoft.Pex.Engine.Drivers;
using Microsoft.Pex.Engine.PostAnalysis;
using Microsoft.Pex.Framework.Packages;

namespace ResultTracking
{
    internal sealed class ResultTracingAttribute
        : PexPathPackageAttributeBase
    {
        protected override object BeforeRun(IPexPathComponent host)
        {
            return null;
        }

        protected override void AfterRun(IPexPathComponent host, object data)
        {
            host.Log.LogMessage("ResultTracing", "begin");

            var controller = new ResultTracer();
            Term[] pathConditions;
            using (IEngine trackingEngine = host.PathServices.TrackingEngineFactory.CreateTrackingEngine(controller))
            {
                trackingEngine.GetService<IPexTrackingDriver>().Run();
                pathConditions = Enumerable.ToArray(controller.PathConditions);
            }

            host.Log.Dump(
                "ResultTracing",
                "conditions checked over all results of uninstrumented methods",
                prettyPrintPathCondition(host, pathConditions));

            host.Log.LogMessage("ResultTracing", "end");
        }

        private static string prettyPrintPathCondition(IPexPathComponent host, Term[] pathConditions)
        {
            var writer = new SafeStringWriter();
            var codeWriter = host.Services.TestManager.Language.CreateBodyWriter(
                writer,
                VisibilityContext.Private,
                100);
            var emitter = new TermEmitter(
                 host.ExplorationServices.TermManager,
                 new NameCreator());
            for (int i = pathConditions.Length - 1; i >= 0; i--)
            {
                var pathCondition = pathConditions[i];
                if (!emitter.TryEvaluate(
                    new Term[] { pathCondition },
                    10000, // bound on size of expression we are going to pretty-print
                    codeWriter))
                {
                    writer.WriteLine("(expression too big; consider using environment variable {0})", ExtendedReflectionEnvironmentSettings.NoCodeEmitterSizeLimit.Name);
                }
                else
                {
                    codeWriter.Return(SystemTypes.Bool);
                }
            }
            return writer.ToString();
        }

        sealed class ResultTracer
            : PexTrackingControllerBase
        {
            #region Don't do anything special with call arguments
            public override void DerivedArguments(int frameId, Method method, Term[] arguments) { }
            public override void FrameDisposed(int frameId, PexTrackingFrame frame) { }
            public override void FrameHasExceptions(int frameId, Method method) { }
            public override void FrameHasExplicitFailures(int frameId, Method method, IEnumerable<object> exceptionObjects) { }
            public override PexArgumentTracking GetArgumentTreatment(PexTrackingThread thread, int frameId, Method method)
            {
                return PexArgumentTracking.Derived;
            }
            public override int GetNextFrameId(int threadId, Microsoft.ExtendedReflection.Metadata.Method method)
            {
                return 0;
            }
            #endregion

            public override PexResultTracking GetResultTreatment(PexTrackingThread thread, int callId, IMethodSignature methodSignature, TypeEx[] varArgTypes, bool hasDerivedResult)
            {
                var method = methodSignature as Method;
                TypeEx declaringType;
                if (method != null &&
                    method.TryGetDeclaringType(out declaringType) &&
                    declaringType == MetadataFromReflection.GetType(typeof(File)))
                    return PexResultTracking.Track; // inject symbols for all methods of System.IO.File
                else
                    return PexResultTracking.ConcreteOrDerived;
            }

            public IEnumerable<Term> PathConditions
            {
                get { return this.PathConditionBuilder.RawConditions; }
            }
        }
    }
}